Add minimal functionality for using GenMC mode #4506

Patrick-6 · 2025-07-29T12:53:21Z

This PR is the MVP for Miri-GenMC, which adds enough functionality to be able to check some simple programs.

A lot of functionality is missing and will be added in future PRs (e.g., atomic read-modify-write/compare_exchange/fences, Mutex support, support for mixed atomic and non-atomic memory accesses to the same location, etc.)
(The commit history shows some of the features that were removed for this PR.)

The current branch uses a fork of GenMC, since are some changes there that must be upstreamed there first. This PR should not be merged until this is finished.

…ptions yet)

- Add genmc-sys crate for building GenMC C++ code. - Implemented program features: - Handling of atomic loads, stores, allocations and deallocations. - Implement consistent address allocations for globals - Non-global addresses allocated by GenMC. - Limitation: No address randomization. - Limitation: No address reuse. - Handling of non-atomic memory accesses. - Limitation: need to split up NA reads and stores into max 8 byte chunks. - Limitation: no mixed size access support. - Limitation: Incomplete (unsound) handling of uninitialized memory. - Implement Pointer conversions to and from GenMC - Limitation: Aliasing model checking must be disabled. - Handling of Read-Modify-Write, Compare-Exchange and Atomic Exchange operations. - Limitation: Compare-Exchange currently ignores possibility of spurious failures. - Limitation: Compare-Exchange failure memory ordering is ignored. - Handling of thread creation and finishing. - Added Miri to GenMC thread id mapping. - Implement mutex lock, try_lock and unlock. - Make use of annotations to reduce number of blocked executions for programs with mutexes. - Add estimation mode for Miri-GenMC. - Limitation: Printing currently handled on C++ side (Should be moved once VerificationResult is available to Rust code) - Thread scheduling in Miri done through GenMC, add loop over eval_entry function. - Rebase GenMC to use new scheduler. - Added GenMC `__VERIFIER_assume` equivalent for Miri (`miri_genmc_verifier_assume`) - Add warnings for GenMC mode for unsupported features. - Add a lot of test, including translation of GenMC litmus tests. - Only run tests if 'genmc' feature enabled. - WIP: try implementing NonNullUniquePtr wrapper for CXX. - WIP: work on mixed atomic/non-atomics. - Partially working, some issues with globals - FIX: Make naming consistent with GenMC for blocked execution Squashed changes: - Add git support to build, move C++ files into genmc-sys crate - Implement building GenMC-Miri after GenMC codebase split. - Cleanup genmc-sys build, remove walkdir dependency. - Fix printing after LLVM IO removal. - WIP: temporarily point GenMC repo to private branch. - WIP: Work on building without LLVM dependency. - Fix build for Ubuntu 22 - Disable stacked borrows for GenMC tests - Get Miri-GenMC building again after rebasing onto GenMC release 0.12.0 - Translate some Loom tests for Miri-GenMC. - Add error for using native-lib with GenMC mode. - Remove on_stack_empty handling except for main thread. - Rename 'stuck' to 'blocked' to be in line with GenMC terminology. - Enable tests that were blocked on rust-lang #116707 - Remove redundant file in compilation step. - Clean up InterpResult<'tcx, ()> - Improve program exit handling, remove 'thread_stack_empty' hack, clean up terminator cache leftovers.

Patrick-6 · 2025-07-29T15:48:45Z

I'll add some comments on the PR later in places that need discussion or that might need to change (since they are based on changes not yet merged into GenMC).

There is also some C++ code that is currently in my fork of GenMC, but makes more sense to move to the Miri repo (e.g., error handling code).

The Rust side should be ready for reviewing.

r? @RalfJung

Patrick-6 · 2025-07-29T18:42:03Z

genmc-sys/src/lib.rs

+    // FIXME(genmc): Rework error handling (likely requires changes on the GenMC side).
+
+    #[must_use]
+    #[derive(Debug)]
+    struct LoadResult {
+        is_read_opt: bool,
+        read_value: GenmcScalar,
+        error: UniquePtr<CxxString>,
+    }
+
+    #[must_use]
+    #[derive(Debug)]
+    struct StoreResult {
+        error: UniquePtr<CxxString>,
+        isCoMaxWrite: bool,
+    }


These will need to be reworked, but I'm waiting on a review of a PR with changes to how GenMC does error handling.

genmc-sys/src/lib.rs

Patrick-6 · 2025-07-29T18:47:43Z

genmc-sys/src/lib.rs

+    #[derive(Debug, Clone, Copy)]
+    struct GenmcScalar {
+        value: u64,
+        is_init: bool,
+    }


We have this type with the is_init flag since CXX doesn't support sending Option (or std::optional) across the language boundary. GenMC only supports up to 64 bit memory accesses, therefore the u64. Lastly, we don't support sending pointers to GenMC in this PR, so no field for provenance information (this also needs some design work on the GenMC side first).

Patrick-6 · 2025-07-29T18:49:15Z

genmc-sys/src_cpp/MiriInterface.cpp

+auto MiriGenMCShim::scheduleNext(const int curr_thread_id,
+								 const ActionKind curr_thread_next_instr_kind) -> int64_t


Discussion topic: naming conventions for Miri C++ code (currently not very consistent).

genmc-sys/src_cpp/MiriInterface.cpp

Patrick-6 · 2025-07-29T18:52:10Z

src/alloc_addresses/mod.rs

+/// FIXME(GenMC): is it ok to make this public?
+pub(crate) fn align_addr(addr: u64, align: u64) -> u64 {


Some code related to memory allocation and threads has been made public in this PR so GenMC can access them.

This is just a little helper, fine to make it public.

But probably we can share some more code if instead we have here something like

pub struct AddressGenerator { next: u64, end: u64, } impl AddressGenerator { pub fn new(addr_range: Range<u64>) -> Self { ... } pub fn generate(&mut self, size: Size, align: Align, rng: &mut ...) -> u64 { ... } }

src/alloc_addresses/mod.rs

Patrick-6 · 2025-07-29T19:00:40Z

src/concurrency/genmc/global_allocations.rs

+    // FIXME(genmc): Decide on an API for GenMC to access this (to check if access to global memory is valid), or decide we don't need that.
+    #[allow(unused)]
+    /// This is used as a map between the address of each allocation and its `AllocId`. It is always
+    /// sorted by address. We cannot use a `HashMap` since we can be given an address that is offset
+    /// from the base address, and we need to find the `AllocId` it belongs to. This is not the
+    /// *full* inverse of `base_addr`; dead allocations have been removed.
+    int_to_ptr_map: Vec<(u64, AllocId)>,


GenMC can ask the interpreter if some address is allocated in the address space for statics (here).

On my branch I've disabled this check. If we want to re-enable, we need to:

decide on an API that is interpreter agnostic (currently it only works with LLI)

somehow allow GenMC to (safely) access this map

It might be easier to just skip this check on the GenMC side with Miri, since Miri should already check if an access is valid or not.

It might be easier to just skip this check on the GenMC side with Miri, since Miri should already check if an access is valid or not.

That's what we should do.

src/concurrency/genmc/global_allocations.rs

src/concurrency/genmc/helper.rs

Patrick-6 · 2025-07-29T19:10:17Z

src/concurrency/genmc/miri_genmc.rs

+    for rep in 0u64.. {
+        tracing::info!("Miri-GenMC loop {}", rep + 1);
+        let result = eval_entry(genmc_ctx.clone());


Random limit of 2^64, we don't actually need that. ^^

I wonder if we should have a print regardless of log level e.g., every 1000 rounds, since test runs can take extremely long, and having zero feedback on the progress is not great.

Patrick-6 · 2025-07-29T19:13:20Z

src/concurrency/thread.rs

+        // FIXME(genmc,question): Is it correct to move this code here?
+        match &mut this.machine.data_race {
+            GlobalDataRaceHandler::None => {}
+            GlobalDataRaceHandler::Vclocks(data_race) =>
+                data_race.thread_terminated(&this.machine.threads),
+            GlobalDataRaceHandler::Genmc(genmc_ctx) => {
+                // Inform GenMC that the thread finished.
+                // This needs to happen once all accesses to the thread are done, including freeing any TLS statics.
+                genmc_ctx.handle_thread_finish(&this.machine.threads)
+            }
+        }


data_race.thread_terminated was getting called before the TLS deallocation before, but I can also happen afterwards I think.
For GenMC, it must happen afterwards, since we shouldn't create any more GenMC events after a thread is finished.

Yeah that makes sense to reorder.

Patrick-6 · 2025-07-29T19:14:20Z

src/concurrency/thread.rs

+                // FIXME(genmc): properly handle sleep in GenMC mode.
                SchedulingAction::Sleep(duration) => {
                    this.machine.monotonic_clock.sleep(duration);
                }


Probably not a problem for this PR, but we need to figure out how to handle sleep (just ignoring sleep might work).

Patrick-6 · 2025-07-29T19:17:31Z

src/eval.rs

+                // In GenMC mode, we let GenMC decide what happens on main thread exit.
+                if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
+                    // If there's no error, execution will continue (on another thread).
+                    genmc_ctx.handle_exit(ThreadId::MAIN_THREAD, exit_code, false)?;
+                } else {
+                    // Stop interpreter loop.
+                    throw_machine_stop!(TerminationInfo::Exit {
+                        code: exit_code,
+                        leak_check: true
+                    });
+                }


This and the change to report_error in diagnostics.rs have replaced my hacks for preventing Miri from exiting when the main thread exits. In GenMC mode, all program exits should use TerminationInfo::GenmcFinishedExecution instead of TerminationInfo::Exit.

Patrick-6 · 2025-07-29T19:20:13Z

tests/genmc/pass/litmus/2+2W+3sc+rel1/2_2w_3sc_rel1.rs

+//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows
+
+#![no_main]
+
+#[path = "../../../../utils-dep/mod.rs"]
+mod utils_dep;
+
+use std::ffi::c_void;
+use std::sync::atomic::{AtomicU64, Ordering};
+
+static X: AtomicU64 = AtomicU64::new(0);
+static Y: AtomicU64 = AtomicU64::new(0);
+
+use crate::utils_dep::*;
+
+#[unsafe(no_mangle)]
+fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
+    let _ids = unsafe { create_pthreads_no_params([thread_1, thread_2]) };
+
+    0
+}


Questions for the tests:

Is there a better way to include the utils-dep than the ../ chain?

How should the includes be handled? Include Ordering or Ordering::*?

Naming: create_pthreads_no_params? spawn_pthreads_no_params?

tests/utils-dep/miri_extern.rs

…ked executions.

tests/genmc/pass/litmus/default/default.order321.stderr

tests/utils-dep/genmc.rs

tests/utils-dep/miri_extern.rs

genmc-sys/src/lib.rs

RalfJung · 2025-07-30T10:10:19Z

genmc-sys/src/lib.rs

+    #[derive(Debug)]
+    enum ActionKind {
+        /// Any Mir terminator that's atomic and has load semantics.
+        Load,


The comment should make it clear that "load" is "maybe load" and "non-load" is "definitely not a load".

genmc-sys/src_cpp/MiriInterface.cpp

RalfJung · 2025-07-30T10:22:52Z

genmc-sys/src/lib.rs

+    #[must_use]
+    #[derive(Debug)]
+    struct LoadResult {
+        is_read_opt: bool,


What does this mean? A comment would be good.

RalfJung · 2025-07-30T10:23:56Z

genmc-sys/src_cpp/MiriInterface.cpp

+
+	auto newLab = std::make_unique<ReadLabel>(pos, ord, loc, aSize, type);
+
+	auto result = GenMCDriver::handleLoad(std::move(newLab));


This might also have to sometimes decrement?

genmc-sys/src_cpp/MiriInterface.hpp

…g prints

…ntal changes.

genmc-sys/src_cpp/MiriInterface.hpp

RalfJung · 2025-07-30T15:11:29Z

genmc-sys/src_cpp/MiriInterface.cpp

+void MiriGenMCShim::handleExecutionStart()
+{
+	globalInstructions.clear();
+	globalInstructions.push_back(Action(ActionKind::Load, Event::getInit()));


Please have a comment explaining that "load" is the conservative choice here.

src/alloc_addresses/mod.rs

tests/genmc/pass/thread/libc_exit.rs.disabled

tests/genmc/pass/thread/thread_simple.rs

tests/genmc/pass/thread/miri_main_spawn_pthreads.rs

RalfJung · 2025-07-30T16:45:11Z

src/concurrency/genmc/mod.rs

+    }
+}
+
+impl GenmcCtx {


These private helpers should have comments.

src/concurrency/genmc/mod.rs

Patrick-6 · 2025-07-31T08:06:00Z

Commit at the time of the current review: a42452b

WIP: Add initial support for running Miri flamegraph (no flamegraph o…

3fc854d

…ptions yet)

rustbot added the S-waiting-on-author Status: Waiting for the PR author to address review comments label Jul 29, 2025

Patrick-6 force-pushed the miri-genmc-mvp branch from 7c34fc3 to 37e652f Compare July 29, 2025 13:53

Patrick-6 added 2 commits July 29, 2025 16:43

Remove duplicate tests

af9d846

Clean up comments.

9d7e964

Patrick-6 force-pushed the miri-genmc-mvp branch from 37e652f to 5104d08 Compare July 29, 2025 15:00

rustbot assigned RalfJung Jul 29, 2025